Nuprl Lemma : duplicate-and
11,40
postcript
pdf
p
,
q
:
. (
p
&
p
&
q
)
(
p
&
q
)
latex
Definitions
Type
,
,
t
T
,
x
:
A
B
(
x
)
,
P
&
Q
,
P
Q
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
origin
p, q:
. (p & p & q) 
(p & q) p, q:. (p & p & q) (p & q) 
T
B(x) Q Q Qx:A. B(x)